/* 
   Model: 		rether.4.m
   Description (short):	Real-time Ethernet Protocol
   Description (long):	Software-based, real-time Ethernet protocol developed at SUNY. Its purpose is to provide guaranteed bandwidth and deterministic, 				periodic network access to multimedia applications over commodity Ethernet hardware. It is a contention-free token bus protocol
			for the datalink layer of the ISO protocol stack.
   Author:		Paolo Bozzelli <paolo.bozzelli@gmail.com>, Giuseppe Cascavilla <g.cascavilla@gmail.com>
*/

CONST
	RT_SLOTS : 3;
	MAX_N : 9;
	SLOTS : 5;

TYPE
	signal : boolean;
	choose : 0..1;
	node_id: 0..2;
	count  : 0..5;
	node_t : enum { idle, start, NRT_action, RT_action, want_RT, error_st, wait_ok, reserved, finish };
	bw_t   : enum { idle, res, rel, error_st };
	token_t: enum { start, NRT_phase, RT_phase, NRT_wait, RT_wait, cycle_end };
	sig_t  : record s:signal; end;
	chan_t : record id:node_id; action:signal; end;
	bwact_t: record node:chan_t; end;
	visit_t: array [ MAX_N ] of sig_t;
	rt_t   : array [ MAX_N ] of choose;

VAR
	/* Real-time nodes counter */
	RT_count : count;

	/* Local variables */
	l_rt : signal;
	l_granted : choose;
	l_nrt_count : count;
	l_i : count; 		-- 'byte i=0;' in Token().
	l_j : count;		-- 'byte i=0;' in Bandwidth().
	l_next : count;
	
	/* Channels */
	reserve : bwact_t;
	release : bwact_t;
	grant : sig_t;
	no_grant : sig_t;
	done : sig_t;
	visit : visit_t;

	/* Processes */
	nodes : array [ MAX_N ] of node_t;
	bandwidth : bw_t;
	token : token_t;

	/* Array of chosen nodes */
	in_RT : rt_t;

/*** TRANSATION RULES ***/

/*** Nodes rules ***/
ruleset i:MAX_N do
	
	/* (node) idle: visit_i?rt : goto start; */
	rule "node - visit" 
		(nodes[i] = idle & visit[i].s) ==>
		BEGIN
			l_rt := visit[i].s;
			nodes[i] := start;					/* ::  visit_0?rt; goto start; */
		END;

	/* (node) start: (rt==1) goto RT_action; */
	rule "node - start - transmitting RT traffic (rt=1)"
		(l_rt && nodes[i] = start) ==>
		BEGIN
			nodes[i] := RT_action;					/* :: (rt == 1); goto RT_action; */
		END;
	
	/* (node) start: (rt==0) goto NRT_action; */
	rule "node - start - transmitting NRT traffic (rt=0)"
		(!l_rt && nodes[i] = start) ==>
		BEGIN
			nodes[i] := NRT_action;					/* :: (rt == 0); goto NRT_action; */
		END;

	rule "node - RT action - Release request"
		(nodes[i] = RT_action & !release.node.action) ==>
		BEGIN
			release.node.id := i;
			release.node.action := true;
			l_granted := 0;
			nodes[i] := finish;					/* :: atomic { release!0; granted = 0; } goto wait_ok; */
		END;

	rule "node - RT action - No release request"
		(nodes[i] = RT_action) ==>
		BEGIN
			if (l_granted = 0)
				nodes[i] := error_st;				/* :: (granted == 0); goto error_st; */
			else
				nodes[i] := finish;				/* :: goto finish; */
			end;		
		END;
	
	rule "node - NRT action"
		(nodes[i] = NRT_action) ==>
		BEGIN
			if (l_granted = 0) then
				reserve.node.id := i;
				reserve.node.action := true;
				nodes[i] := want_RT;				/* :: atomic {granted==0;reserve!0;}  goto want_RT; */
			else
				nodes[i] := finish;				/* :: goto finish; */
		END;

	rule "node - want_RT - traffic RT granted"
		(nodes[i] = want_RT & grant.s) ==>
		BEGIN
			nodes[i] := reserved;					/* :: grant?0; goto reserved; */
		END;
	
	rule "node - want_RT - traffic RT not granted"
		(nodes[i] = want_RT & no_grant.s) ==>
		BEGIN
			nodes[i] := finish;					/* :: no_grant?0; goto finish; */
		END;
	
	rule "node - reserved"
		(nodes[i] = reserved) ==>
		BEGIN
			l_granted := 1;
			nodes[i] := finish;					/* :: granted = 1; goto finish; */
		END;

	rule "node - finish"
		(nodes[i] = finish) ==>
		BEGIN
			done.s := true;
			nodes[i] := idle;					/* :: done!0; goto idle; */
		END;

	rule "node - error_st"
		(nodes[i] = error_st) ==>
		BEGIN
			assert(false);						/* error_st : false; */
		END;

END; -- ruleset
/* END $ Nodes RULES */

/* BEGIN $ Token rules */
	
	rule "token - idle"
		(token = start) ==>
		BEGIN
			l_i = 0;
			token := RT_phase;					/* :: i = 0; goto RT_phase; */
		END;
	
	rule "token - RT_phase - l_i < MAX_N"
		(token = RT_phase & l_i < MAX_N) ==>
		BEGIN
			switch (in_RT[l_i])
				case 0: l_i := l_i + 1; token := RT_phase;	/* :: d_step {i<9 && in_RT[i]==0;i = i+1;}  goto RT_phase; */
				case 1: visit[l_i].s := true; token := RT_wait;	/* ::  atomic {i==§ && in_RT[i]==1;visit_§!1;}  goto RT_wait; */
			end; --switch
		END;
			
	rule "token - RT_phase - l_i = MAX_N"
		(token = RT_phase & l_i = MAX_N)
		BEGIN
			token := NRT_phase;					/* :: i==3; goto NRT_phase; */
		END;

	rule "token - RT_wait"
		(token = RT_wait & done.s) ==>
		BEGIN
			l_i := l_i + 1;
			token := RT_phase;					/* :: atomic {done?0;i = i+1;}  goto RT_phase; */
		END;

	rule "token - NRT_phase (NRT_count > 0)"
		(token = NRT_phase & NRT_count > 0) ==>
		BEGIN
			switch (l_next)
				case 0: visit[0].s := false; token := NRT_wait;	/* :: atomic {NRT_count>0 && next==0;visit_0!0;}  goto NRT_wait; */
				case 1: visit[1].s := false; token := NRT_wait;	/* :: atomic {NRT_count>0 && next==1;visit_1!0;}  goto NRT_wait; */
				case 2: visit[2].s := false; token := NRT_wait;	/* :: atomic {NRT_count>0 && next==2;visit_2!0;}  goto NRT_wait; */
				case 3: visit[3].s := false; token := NRT_wait;	/* :: atomic {NRT_count>0 && next==3;visit_3!0;}  goto NRT_wait; */
				case 4: visit[4].s := false; token := NRT_wait;	/* :: atomic {NRT_count>0 && next==4;visit_4!0;}  goto NRT_wait; */
				case 5: visit[5].s := false; token := NRT_wait;	/* :: atomic {NRT_count>0 && next==5;visit_5!0;}  goto NRT_wait; */
				case 6: visit[6].s := false; token := NRT_wait;	/* :: atomic {NRT_count>0 && next==6;visit_6!0;}  goto NRT_wait; */
				case 7: visit[7].s := false; token := NRT_wait;	/* :: atomic {NRT_count>0 && next==7;visit_7!0;}  goto NRT_wait; */
				case 8: visit[8].s := false; token := NRT_wait;	/* :: atomic {NRT_count>0 && next==8;visit_8!0;}  goto NRT_wait; */
			end;
		END;
	
	rule "token - NRT_phase (NRT_count = 0)"
		(token = NRT_phase & NRT_count = 0) ==>
		BEGIN
			token := cycle_end;					/* :: NRT_count == 0; goto cycle_end; */
		END;

	rule "token - NRT_wait"
		(token = NRT_wait & done.s) ==>
		BEGIN
			l_next := (l_next + 1) % MAX_N;
			NR_count := NR_count + 1;
			token := NRT_phase;					/* :: atomic {done?0;next = (next+1)%9;NRT_count = NRT_count-1;} goto NRT_phase;  */
		END;
	
	rule "token - cycle end"
		(token = cycle_end) ==>
		BEGIN
			NRT_count = SLOTS - NRT_count;				
			token = start;						/* :: NRT_count = 3-NRT_count; goto start; */
		END;

/* END $ Token rules */

/* BEGIN $ Bandwidth rules */

	rule "bw - idle -> release"
		(bandwidth = idle & release.node.action) ==>
		BEGIN
			l_j := release.node;
			release.node.action := false;
			bandwidth := rel;					/* :: release?i; goto rel; */
		END;

	rule "bw - idle -> reserve"
		(bandwidth = idle & reserve.node.action) ==>
		BEGIN
			l_j := reserve.node;
			reserve.node.action := false;
			bandwidth := res;					/* :: reserve?i; goto res; */
		END;
	
	rule "bw - release - in_RT[i] = 1"
		(bandwidth = rel & in_RT[l_j] = 1) ==>
		BEGIN
			in_RT[l_j] := 0;
			RT_count := RT_count - 1;
			bandwidth := idle;					/* :: atomic {in_RT[i]==1;in_RT[i] = 0;RT_count = RT_count-1;}  goto idle; */
		END;
	
	rule "bw - release - in_RT[i] = 0"
		(bandwidth = rel & in_RT[l_j] = 0) ==>
		BEGIN
			bandwidth := error_st;					/* :: in_RT[i]==0; goto error_st; */
		END;

	rule "bw - reserve - RT_count >= RT_SLOTS"
		(bandwidth = res & RT_count >= RT_SLOTS) ==>
		BEGIN
			no_grant.s := true;
			bandwidth := idle;					/* :: atomic {RT_count>=2;no_grant!0;}  goto idle; */
		END;
		
	rule "bw - reserve - RT_count < RT_SLOTS"
		(bandwidth = res & RT_count < RT_SLOTS) ==>
		BEGIN
			grant.s := true;
			RT_count := RT_count + 1;
			in_RT[l_j] := 1;
			reserve.node.action := false;
			bandwidth := idle;					/* :: atomic {RT_count<2;grant!0;RT_count = RT_count+1;in_RT[i] = 1;}  goto idle; */
		END;

	rule "bw - error state"
		(bandwidth = error_st) ==>
		BEGIN
			assert(false);						/* error_st : false; */
		END;

/* END $ Bandwidth rules */

STARTSTATE
	BEGIN
	token := start;
	bandwidth := idle;

	for k:MAX_N do
		nodes[k] := idle;
		in_RT[k] := 0;
	end;

	l_granted := 0;
	l_rt := false;
	l_nrt_count := SLOTS;
	END;

INVARIANT
	!exists i:MAX_N do
		(nodes[i] = error_st)
	end;
